{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}

module T where

import TypeBasics (encode)
import TypeSums (inject)
import Yoko



data Occ = Par Int | Env Int
instance Show Occ where
  show (Env i) = '^' : show i
  show (Par i) = show i

data TLF = Occ Occ | Top Int [Occ] | App TLF TLF
  deriving Show

type Dec = (Int, Int, TLF)
data Prog = Prog [Dec] TLF deriving Show





data Occ_ = Occ_ Occ
data Top_ = Top_ Int [Occ]
data App_ = App_ TLF TLF



type instance Range Occ_  = TLF
type instance Range Top_ = TLF
type instance Range App_  = TLF

type instance Tag Occ_ = $(return $ encode "Occ")
type instance Tag Top_ = $(return $ encode "Top")
type instance Tag App_  = $(return $ encode "App")

concat `fmap` mapM derive [''TLF, ''Occ, ''Occ_, ''Top_, ''App_]



type instance Rep Occ_ = Dep Occ
instance Generic Occ_ where
  rep (Occ_ o) = Dep o
  obj (Dep o)  = Occ_ o
type instance Rep Top_ = Dep Int :*: Dep [Occ]
instance Generic Top_ where
  rep (Top_ i os)        = Dep i :*: Dep os
  obj (Dep i :*: Dep os) = Top_ i os
type instance Rep App_ = Rec TLF :*: Rec TLF
instance Generic App_ where
  rep (App_ tm1 tm2) = Rec tm1 :*: Rec tm2
  obj (Rec tm1 :*: Rec tm2) = App_ tm1 tm2



type instance DCs TLF = N Occ_ :+: N Top_ :+: N App_
instance DT TLF where
  disband (Occ i)       = DCsOf . inject $ Occ_ i
  disband (Top i os)    = DCsOf . inject $ Top_ i os
  disband (App tm1 tm2) = DCsOf . inject $ App_ tm1 tm2
instance DC Occ_ where rejoin (Occ_ i)       = Occ i
instance DC Top_ where rejoin (Top_ i os)    = Top i os
instance DC App_ where rejoin (App_ tm1 tm2) = App tm1 tm2
